(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun q () Real)
(declare-fun s () Real)
(assert (exists ((r Real)) (or (= m 0) (< 0 (* b m)) (<= 0 s) (< 0 d) (=> (> r l 0 (* (/ 9 m) r)) (= f 2)))))
(assert (forall ((p Real)) (and (or (and (= 0 (+ (/ j n) g)) (> (/ k (/ (+ (* j j) (* (- c s) (+ 126 c)) (* g (- (+ (/ 2 k) s) g))) (* (* j (- 173 c s)) (+ (* k (* 8 c s)) (* 2 g))))) 0)) (= q 0) (>= 0 j) (< 0 (/ 2 e) 0)) (< (/ (* (/ 1 9) (* g o)) (/ (* (+ (* j i) g) (/ 7 (* j (/ a i)) g)) 0)) h))))
(check-sat)
